\documentclass[10pt,a4paper]{report}
\usepackage[top=3cm, bottom=2.5cm, left=3cm, right=2.5cm] {geometry}
\usepackage {bsymb,b2latex}
\usepackage{fancyhdr,lastpage}
\lhead{\rm An Event-B Specification of variables}
\rhead {\rm Page \thepage~of \pageref{LastPage}}
\lfoot{}\cfoot{}\rfoot{}
\pagestyle{fancy}
%---------------------------------------------------------
\begin{document}
\thispagestyle{empty}
\begin{description}
\BTitle{variables}{27 Jul 2008}{09:36:48 PM}
\MACHINE{variables}
\SEES{constantes14}
\VARIABLES
	\begin{description}
		\Item{ pp }
		\Item{ pc }
	\end{description}
\INVARIANTS
	\begin{description}
		\nItem{ inv4 }{ personas \neq  \emptyset  }
		\nItem{ inv1 }{ pp \subseteq   personas  }
		\cmt{ personas pagando	 }
		\nItem{ inv2 }{ pc \subseteq  personas }
		\cmt{ personas comprando }
		\nItem{ inv3 }{ pc \binter  pp = \emptyset   }
		\cmt{ las personas que pagan tener encuenta que no pueden tener cosas en comun }
	\end{description}
\EVENTS
	\INITIALISATION
		\begin{description}
		\Begin
			\begin{description}
			\nItem{ act1 }{ pp := \emptyset  }
			\nItem{ act2 }{ pc :=  \emptyset  }
			\end{description}
		\End
		\end{description}
	\EVT {entra}
		\begin{description}
		\Any
			\begin{description}
			\Item{ p }
			\end{description}
		\Where
			\begin{description}
			\nItem{ grd1 }{ p \in  personas }
			\nItem{ grd2 }{ p \notin  (pc \bunion  pp) }
			\end{description}
		\Then
			\begin{description}
			\nItem{ act1 }{ pc :=  pc \bunion \{ p\}  }
			\end{description}
		\End
		\end{description}
	\EVT {salir}
		\begin{description}
		\Any
			\begin{description}
			\Item{ p }
			\end{description}
		\Where
			\begin{description}
			\nItem{ grd1 }{ p \in  pp  }
			\end{description}
		\Then
			\begin{description}
			\nItem{ act1 }{ pp :=   pp\setminus \{ p\}   }
			\end{description}
		\End
		\end{description}
	\EVT {pasar}
		\begin{description}
		\Any
			\begin{description}
			\Item{ p }
			\end{description}
		\Where
			\begin{description}
			\nItem{ grd1 }{ p \in   pc }
			\nItem{ grd2 }{ p\notin  pp }
			\end{description}
		\Then
			\begin{description}
			\nItem{ act2 }{ pc :=  pc  \setminus \{ p\}  }
			\nItem{ act1 }{ pp :=  pp \bunion  \{ p\}  }
			\end{description}
		\End
		\end{description}
\END
\end{description}
\end{document}
